nLab geometric homotopy type theory

Idea

As geometric type theory refers to a conjectural extension of geometric logic to an extensional dependent type theory that corresponds to sheaf toposes (under the relation between category theory and type theory) with geometric morphisms between them, a similar conjectural extension to a homotopy type theory corresponding to (∞,1)-sheaf (∞,1)-toposes (and geometric morphisms) maybe deserves to be called geometric homotopy type theory.

Since homotopy colimits are preserved by inverse images of geometric morphisms, this type theory is likely to include at least non-recursive higher inductive types, and furthermore perhaps free models for every (finite) essentially algebraic (infinity,1)-theory. (Arbitrary recursive higher inductive types only make sense with reference to Pi-types, which are not geometric.)

Traditionally the types in geometric homotopy type theory, hence the geometric homotopy types, are known as ∞-stacks and maybe better as (∞,1)-sheaves, notably as moduli ∞-stacks.

Examples

• geometrically discrete homotopy type

• smooth homotopy type

• smooth super homotopy type

Related concepts

• geometric mathematics

• linear type theory

• modal homotopy type theory

• cohesive homotopy type theory

• directed homotopy type theory

• stable homotopy type